\begin{tabbing}
with declarations 
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]$k$(v) sends $f$ s v on link $l$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ma\{\=${\it ds}$;\+
\\[0ex]${\it da}$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$;
\\[0ex]$<$$k$, $l$$>$ : $f$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$;
\\[0ex]$\otimes$\}
\-
\end{tabbing}